package joc.nextgen.dbi;

import static joc.nextgen.JOC.old;
import static joc.nextgen.JOC.result;
import joc.nextgen.dbi.JOC.PostCondition;
import joc.nextgen.dbi.JOC.PreCondition;

public class StackSpecContract<T> implements StackSpec<T> {
	@Override
	public int size() {
		new PostCondition() {
			{
				assert result(Integer.class) >= 0;
			}
		};
		return 0; // notwendig wegen implements
	}

	@Override
	public void pop() {
		new PreCondition() {
			{
				assert size() > 0;
			}
		};
		new PostCondition() {
			{
				assert size() == old(size()) - 1;
				assert top() == old(get(2));
			}
		};
	}

	@Override
	public T get(final int i) {
		new PreCondition() {
			{
				assert !isEmpty();
				assert i > 0;
				assert size() >= i;
			}
		};
		new PostCondition() {
			{
				assert result() != null;
			}
		};
		return null;
	}

	@Override
	public boolean isFull() {
		return false;
	}

	@Override
	public boolean isEmpty() {
		return false;
	}

	@Override
	public T top() {
		new PreCondition() {
			{
				assert size() > 0;
			}
		};
		new PostCondition() {
			{
				assert size() == old(size());
			}
		};
		return null;
	}

	@Override
	public void push(final T elem) {
		new PreCondition() {
			{
				assert !isFull();
			}
		};
		new PostCondition() {
			{
				assert size() == old(size()) + 1;
				assert top() == elem;
			}
		};
	}
}